Problem:
 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(x1))))))))))
 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(x1)))))))))))))
 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))
 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))
 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))

Proof:
 Bounds Processor:
  bound: 2
  enrichment: match
  automaton:
   final states: {3}
   transitions:
    11(22) -> 23*
    11(24) -> 25*
    11(19) -> 20*
    11(21) -> 22*
    11(16) -> 17*
    21(15) -> 16*
    21(32) -> 33*
    21(26) -> 27*
    21(23) -> 24*
    21(18) -> 19*
    01(20) -> 21*
    01(17) -> 18*
    12(52) -> 53*
    12(54) -> 55*
    12(49) -> 50*
    12(51) -> 52*
    12(46) -> 47*
    00(2) -> 3*
    00(1) -> 3*
    22(60) -> 61*
    22(45) -> 46*
    22(58) -> 59*
    22(53) -> 54*
    22(48) -> 49*
    10(2) -> 1*
    10(1) -> 1*
    02(50) -> 51*
    02(47) -> 48*
    20(2) -> 2*
    20(1) -> 2*
    1 -> 26*
    2 -> 15*
    21 -> 32*
    24 -> 45*
    25 -> 18,3
    27 -> 16*
    33 -> 19*
    51 -> 58*
    54 -> 60*
    55 -> 21,32
    59 -> 49*
    61 -> 46*
  problem:
   
  Qed